/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * sygus_term_enumerator
 */

#include "cvc5_private.h"

#ifndef CVC5__EXPR__SYGUS_TERM_ENUMERATOR_H
#define CVC5__EXPR__SYGUS_TERM_ENUMERATOR_H

#include <unordered_set>

#include "expr/node.h"
#include "expr/type_node.h"
#include "smt/env_obj.h"

namespace cvc5::internal {

namespace theory::quantifiers {
class SygusEnumerator;
}
/**
 * A virtual callback for whether to consider terms in an enumeration.
 */
class SygusTermEnumeratorCallback
{
 public:
  SygusTermEnumeratorCallback() {}
  virtual ~SygusTermEnumeratorCallback() {}
  /**
   * Add term, return true if the term should be considered in the enumeration.
   * Notice that returning false indicates that n should not be considered as a
   * subterm of any other term in the enumeration.
   *
   * @param n The SyGuS term, which is a deep embedding of the next term to
   * enumerate.
   * @param bterms The (rewritten, builtin) terms we have already enumerated
   * @return true if n should be considered in the enumeration.
   */
  virtual bool addTerm(const Node& n, std::unordered_set<Node>& bterms) = 0;
};

/**
 * SygusTermEnumerator
 *
 * This class is used for enumerating all terms of a sygus datatype type. At
 * a high level, it is used as an alternative approach to sygus datatypes
 * solver as a candidate generator in a synthesis loop. It filters terms based
 * on redundancy criteria, for instance, it does not generate two terms that can
 * be shown to be equivalent via rewriting. It enumerates terms whose deep
 * embedding is considered in order of sygus term size
 * (TermDb::getSygusTermSize).
 *
 * It also can be configured to enumerate sygus terms with free variables,
 * (as opposed to variables bound in the formal arguments list of the
 * function-to-synthesize), where each free variable appears in exactly one
 * subterm. For grammar:
 *   S -> 0 | 1 | x | S+S
 * this enumerator will generate the stream:
 *   z1, 0, 1, x, z1+z2, z1+1, 1+1 ...
 * and so on, where z1 and z2 are variables of type Int. We call
 * these "shapes". This feature can be enabled by setting enumShapes to true
 * in the constructor below.
 *
 * In detail to generate all terms in a grammar:
 *
 *   SygusTermEnumerator enum(...);
 *   std::vector<Node> terms;
 *   do
 *   {
 *     terms.push_back(enum.getCurrent());
 *   } while (enum.increment());
 */
class SygusTermEnumerator
{
 public:
  /**
   * @param env Reference to the environment
   * @param tn The sygus datatype that encodes the grammar
   * @param sec Pointer to an (optional) callback, required e.g. if we wish to
   * do conjecture-specific symmetry breaking
   * @param enumShapes If true, this enumerator will generate terms having any
   * number of free variables
   * @param enumAnyConstHoles If true, this enumerator will generate terms where
   * free variables are the arguments to any-constant constructors.
   * @param numConstants The number of interpreted constants to consider for
   * each size in any-constant constructors.
   */
  SygusTermEnumerator(Env& env,
                      const TypeNode& tn,
                      SygusTermEnumeratorCallback* sec = nullptr,
                      bool enumShapes = false,
                      bool enumAnyConstHoles = false,
                      size_t numConstants = 5);
  ~SygusTermEnumerator() {}
  /**
   * Increment. If true, we ensure that getCurrent() is non-null. If false,
   * there are no more terms in the enumeration.
   */
  bool increment();
  /**
   * Increment partial. Same as above but does not guarantee that getCurrent
   * is non-null. This method can be used if the user wants the enumerator
   * to not put too much effort into trying to enumerate the next value.
   */
  bool incrementPartial();
  /**
   * Get the current term generated by this class. This can be non-null
   * prior to the first call to increment.
   *
   * In particular, this returns the builtin equivalent of the current sygus
   * datatype term that was enumerated.
   */
  Node getCurrent();

 private:
  /** The internal implementation */
  std::unique_ptr<theory::quantifiers::SygusEnumerator> d_internal;
  /** The enumerator, a dummy skolem passed to the above class */
  Node d_enum;
};

}  // namespace cvc5::internal

#endif /* CVC5__EXPR__SYGUS_TERM_ENUMERATOR_H */
